\begin{tabbing}
d{-}world{-}state($D$;$i$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=d{-}m($D$; $i$).state\+
\\[0ex]$\times$Action(d{-}decl($D$;$i$))
\\[0ex]$\times$(\{$m$:d{-}m($D$; $i$).Msg$\mid$ source(mlnk($m$)) $=$ $i$ $\in$ Id \} List)
\-
\end{tabbing}